/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=NGR25

␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY

␈↓ ↓H␈↓CS206  ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS  ␈↓ 
SPRING 1978

␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  2
␈↓ ↓H␈↓␈↓ ¬rDue  May 16


␈↓ ↓H␈↓αGeneral comments.

␈↓ ↓H␈↓        This␈α⊂assignment␈α⊂involves␈α∂proving␈α⊂properties␈α⊂of␈α∂LISP␈α⊂functions.␈α⊂ Unless␈α⊂otherwise␈α∂noted
␈↓ ↓H␈↓your␈α∪proofs␈α∪should␈α∪be␈α∪fairly␈α∪formal.␈α∪ The␈α∪level␈α∪of␈α∪detail␈α∪should␈α∪be␈α∪approximately␈α∀that␈α∪of
␈↓ ↓H␈↓Chapter III␈αsection 7␈αof␈αthe␈αnotes.␈α For␈αeach␈αstep␈αof␈αyour␈αproof,␈αmake␈αsure␈αthat␈αyou␈αlist␈αall␈αof␈αthe
␈↓ ↓H␈↓facts␈α
(axioms,␈αearlier␈α
steps␈α
or␈αpreviously␈α
proved␈α
properties)␈αthat␈α
are␈α
necessary␈αto␈α
make␈α
that␈αstep.
␈↓ ↓H␈↓You may use any facts already proved in the notes or in class.


␈↓ ↓H␈↓αAssignment.

␈↓ ↓H␈↓1. Chapter III.  Exercise 1. ii-v.

␈↓ ↓H␈↓2. Chapter III.  Exercise 2.

␈↓ ↓H␈↓3.␈α
EXTRA␈α(for␈α
practice␈α
with␈αextended␈α
truth␈αvalues,␈α
not␈α
required).␈α Let␈α
␈↓↓andlist␈↓␈αbe␈α
as␈α
defined␈αin
␈↓ ↓H␈↓␈↓ α(Chapter I and assume ␈↓↓p␈↓ is a suitably well-behaved predicate.  Prove the following:

␈↓ ↓H␈↓        3.1. ␈↓↓∀u v: [andlis[u*v, p] = andlis[u, p] ∧ andlis[v, p]]␈↓

␈↓ ↓H␈↓        3.2. ␈↓↓∀u: [andlis[reverse u, p] = andlis[u, p]]␈↓

␈↓ ↓H␈↓Hint:␈αdefine␈α␈↓↓aandlis,␈↓␈αwhich␈αreturns␈αan␈αextended␈αtruth␈αvalue␈αcorresponding␈αto␈αthe␈αtruth␈αvalue␈αof
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis␈↓␈α⊃on␈α⊃corresponding␈α⊃arguments.␈α⊃ Show␈α⊃that␈α⊃␈↓↓andlis␈α⊃as␈↓␈α⊃defined␈α⊃in␈α⊃terms␈α∩of␈α⊃␈↓↓aandlis␈↓
␈↓ ↓H␈↓␈↓ α(satisfies␈αthe␈αdesired␈αequivalence.␈α Then␈αyou␈αmay␈αuse␈αthis␈αresult␈αto␈αprove␈αother␈αfacts␈αabout
␈↓ ↓H␈↓␈↓ α(␈↓↓andlis.␈↓␈α The␈α
statement␈αthat␈α
"␈↓↓p␈↓␈αis␈αsuitably␈α
well-behaved"␈αis␈α
rather␈αvague.␈α
 You␈αwill␈αneed␈α
to
␈↓ ↓H␈↓␈↓ α(make it more precise in order to make your proof clear.   State this  in your proof.